EventsWithKinds
== E:Type
== EqDecider(E)
== Top
== pred?:(E(E+Unit))
== info:(E(IdId+(IdLnkE)Id))
== EOrderAxioms(E; pred?; info)
== T:(IdIdType)
== when:(x:Ide:ET(loc(e),x))
== after:(x:Ide:ET(loc(e),x))
== (e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))))
== Top 

latex

---

clarification:

EKind{i:l}
== E:Type{i}
== EqDecider(E)
== Top
== pred?:(E(E+Unit))
== info:(E(IdId+(IdLnkE)Id))
== EOrderAxioms{i}(E;
== EOpred?;
== EOinfo)
== T:(IdIdType{i})
== when:(x:Ide:ET(loc(info;e),x))
== after:(x:Ide:ET(loc(info;e),x))
== (e:E. first(pred?;e)  (x:Id. when(x,e) = after(x,pred(pred?;e))  T(loc(info;e),x)))
== Top 

latex

Definitions	EventsWithKinds, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), P  Q, A, b, first(e), x:A. B(x), Id, loc(e), pred(e), Top
FDL editor aliases	EKind